.. SPDX-License-Identifier: GPL-2.0 or GPL-3.0
.. Copyright © 2019 Ariadne Devos

Specifying and proving programs
===============================
For formally proving programs correct, annotations in ACSL
are interwoven with the source code, which can be fed into
Frama-C for submission to automatic theorem provers.

A specification of ACSL is available on https://frama-c.com,
as is the free-software Frama-C platform (both GUI and CUI).
A few guidelines are given.

Contracts
---------
The contract of a function is given where it is declared:
the header file for exported functions. If a proposition
is conditional on presence or absence of :ref:`speculation <speculation>`,
this is modelled as being conditional on `S` or `NS` respectively,
defined in `<sHT/nospec.h> `.

Lemmas
------
Invariants' names are suffixed by `I`, before any speculation suffix.

Loops
-----
Specify relevant invariants, the frame (`assigns:`) and `variant:`
for proving termination (if applicable). Frama-C cannot guess
the invariants or the frame, and typically has little trouble
proving them, but only if they are correct.
